rw(Lean 4)
rw(Lean 4)
rewrite タクティク
code:lean
-- one_eq_succ_zeroは1をsucc 0に書き換える定理
-- 1をsucc 0に書き換える
rw
one_eq_succ_zero
-- succ 0を1に戻す
rw
← one_eq_succ_zero
確認用
Q. rw(Lean 4)
調査用
Google.icon
rw(Lean 4)(日)
Google.icon
Rw(lean 4)(英)
Wikipedia.icon
rw(Lean 4) - Wikipedia(日)
rw(Lean 4)(検索) - Wikipedia(日)
Wikipedia.icon
Rw(lean 4) - Wikipedia(英)
Rw(lean 4)(検索) - Wikipedia(英)